Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows
Identifieur interne : 001450 ( Main/Exploration ); précédent : 001449; suivant : 001451Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows
Auteurs : Clara Bertolissi [France, Italie] ; Silvio Ranise [Italie]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We introduce a class of symbolic transition systems capable of representing collections of security-aware workflows and we study the verification of reachability properties of such systems. More precisely, we define composed array-based systems as an extension of array-based systems in which array variables are indexed over more than one type. For an application relevant sub-class of these systems we show how to mechanize a symbolic backward reachability procedure by modularly re-using the techniques developed for array-based systems. Finally, and most importantly, we find sufficient conditions for the termination of the procedure and we apply this result to derive the decidability of the reachability problems of two important classes of security-aware workflow systems.
Url:
DOI: 10.1007/978-3-642-40885-4_4
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003543
- to stream Istex, to step Curation: 003501
- to stream Istex, to step Checkpoint: 000076
- to stream Main, to step Merge: 001462
- to stream Main, to step Curation: 001450
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows</title><author><name sortKey="Bertolissi, Clara" sort="Bertolissi, Clara" uniqKey="Bertolissi C" first="Clara" last="Bertolissi">Clara Bertolissi</name></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E02E73F87B5B8A6A8C9437967CF2C5C05D3F730D</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-40885-4_4</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-7F147WNM-4/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003543</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003543</idno><idno type="wicri:Area/Istex/Curation">003501</idno><idno type="wicri:Area/Istex/Checkpoint">000076</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000076</idno><idno type="wicri:doubleKey">0302-9743:2013:Bertolissi C:verification:of:composed</idno><idno type="wicri:Area/Main/Merge">001462</idno><idno type="wicri:Area/Main/Curation">001450</idno><idno type="wicri:Area/Main/Exploration">001450</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows</title><author><name sortKey="Bertolissi, Clara" sort="Bertolissi, Clara" uniqKey="Bertolissi C" first="Clara" last="Bertolissi">Clara Bertolissi</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LIF-CNRS, UMR 7279 & AMU, Marseille</wicri:regionArea><placeName><region type="region">Provence-Alpes-Côte d'Azur</region><region type="old region">Provence-Alpes-Côte d'Azur</region><settlement type="city">Marseille</settlement></placeName></affiliation><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>FBK (Fondazione Bruno Kessler), Trento</wicri:regionArea><wicri:noRegion>Trento</wicri:noRegion></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>FBK (Fondazione Bruno Kessler), Trento</wicri:regionArea><wicri:noRegion>Trento</wicri:noRegion></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We introduce a class of symbolic transition systems capable of representing collections of security-aware workflows and we study the verification of reachability properties of such systems. More precisely, we define composed array-based systems as an extension of array-based systems in which array variables are indexed over more than one type. For an application relevant sub-class of these systems we show how to mechanize a symbolic backward reachability procedure by modularly re-using the techniques developed for array-based systems. Finally, and most importantly, we find sufficient conditions for the termination of the procedure and we apply this result to derive the decidability of the reachability problems of two important classes of security-aware workflow systems.</div></front></TEI><affiliations><list><country><li>France</li><li>Italie</li></country><region><li>Provence-Alpes-Côte d'Azur</li></region><settlement><li>Marseille</li></settlement></list><tree><country name="France"><region name="Provence-Alpes-Côte d'Azur"><name sortKey="Bertolissi, Clara" sort="Bertolissi, Clara" uniqKey="Bertolissi C" first="Clara" last="Bertolissi">Clara Bertolissi</name></region></country><country name="Italie"><noRegion><name sortKey="Bertolissi, Clara" sort="Bertolissi, Clara" uniqKey="Bertolissi C" first="Clara" last="Bertolissi">Clara Bertolissi</name></noRegion><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001450 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001450 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:E02E73F87B5B8A6A8C9437967CF2C5C05D3F730D
|texte= Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows
}}
| This area was generated with Dilib version V0.6.33. |  |